$\forall$$A$:Realizer, $i$, $x$:Id, $k$:Knd, ${\it test}$:(State(R{-}state($A$;$i$))$\rightarrow$Valtype(R{-}da($A$;$i$);$k$)$\rightarrow\mathbb{B}$).
\\[0ex]R{-}Feasible($A$)
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$$x$ $\in$ dom(R{-}state($A$;$i$))))
\\[0ex]$\Rightarrow$ ($\uparrow$hasloc($k$;$i$))
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$write{-}restricted($A$;$i$;$k$)))
\\[0ex]$\Rightarrow$ ($\forall$$y$:Id. ($\uparrow$$y$ $\in$ dom($x$ : $\mathbb{B}$ $\oplus$ R{-}state($A$;$i$))) $\Rightarrow$ ($\neg$($\uparrow$read{-}restricted($A$; $i$; $y$))))
\\[0ex]$\Rightarrow$ $A$ $\parallel$ R{-}base{-}recognize($i$;R{-}state($A$;$i$);$x$;$k$;Valtype(R{-}da($A$;$i$);$k$);${\it test}$)